package com.cltolarva;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;

import clanalyser.CLAnalyser;
import clanalyser.contract.Clause;

/*
 * Conflict checking in CL
 */

public class NewClToLarvaConverter {

	CLAnalyser appAnalyser;

	public NewClToLarvaConverter() {

		appAnalyser = new CLAnalyser();

	}

	public static void main(String[] args) {

		NewClToLarvaConverter nclc = new NewClToLarvaConverter();

		String generatedLarvaFileName = System.getProperty("user.dir").concat(
				"\\PropertiesInLarva.lrv");

		/*nclc.writeLarvaScript(
				"D:\\JavaConCommandline2012\\PropertiesInLarva.lrv",
				"D:\\JavaConCommandline2012\\CL_CONTRACT.txt",
				"D:\\JavaConCommandline2012");*/
		nclc.writeLarvaScriptTemp(
				"D:\\JavaConCommandline2012\\PropertiesInLarva.lrv",
				"D:\\JavaConCommandline2012\\CL_CONTRACT.txt",
				"D:\\JavaConCommandline2012");

		// nclc.writeLarvaScript(generatedLarvaFileName,args[0]);

		System.out.print("Finish writing larva script");

	}

	public void writeLarvaScript(String fileName, String clContractFile,
			String javaSystemRoot) {

		StringBuilder sb = new StringBuilder();

		try {

			sb.append("IMPORTS\n");// IMPORT START
			sb.append("{\n");
			// this line need to be dynamic
			// sb.append("import test.java;\n");

			sb.append(this.addImports(javaSystemRoot));

			sb.append("}\n");// IMPORT END

			sb.append("GLOBAL\n");// GLOBAL START
			sb.append("{\n");

			sb.append("VARIABLES");// VARIABLES START
			sb.append("{\n");
			// this line need to be dynamic

			// sb.append("int userCnt = 0;\n");

			sb.append(this.addChannel(clContractFile));

			sb.append(this.addControllVariable(clContractFile));

			sb.append("}\n");// VARIABLES END

			sb.append("EVENTS");// EVENTS START
			sb.append("{\n");
			// this line need to be dynamic

			// sb.append("addUser() = {*.addUser()}\n");

			sb.append(this.addGlobalEvents(clContractFile));

			sb.append("}\n");// EVENTS END

			sb.append(this.addControllAutometa(clContractFile));
			sb.append("\n");

			sb.append(this.addAllmonitors(clContractFile));// PROPERTY START
			sb.append("\n");

			sb.append("}\n");// GLOBAL END

			FileWriter fstream = new FileWriter(fileName);
			BufferedWriter out = new BufferedWriter(fstream);
			out.write(sb.toString());
			// Close the output stream
			out.close();

		} catch (Exception e) {
			e.printStackTrace();
		}

	}
	
	public void writeLarvaScriptTemp(String fileName, String clContractFile,
			String javaSystemRoot) {

		StringBuilder sb = new StringBuilder();

		try {

			sb.append("IMPORTS\n");// IMPORT START
			sb.append("{\n");
			// this line need to be dynamic
			// sb.append("import test.java;\n");

			sb.append(this.addImports(javaSystemRoot));

			sb.append("}\n");// IMPORT END

			sb.append("GLOBAL\n");// GLOBAL START
			sb.append("{\n");

			sb.append("\tVARIABLES");// VARIABLES START
			sb.append("{\n");
			// this line need to be dynamic

			// sb.append("int userCnt = 0;\n");

			sb.append(this.addChannel(clContractFile));

			sb.append(this.addControllVariable(clContractFile));

			sb.append("\t}\n");// VARIABLES END

			sb.append("\tEVENTS");// EVENTS START
			sb.append("{\n");
			// this line need to be dynamic

			// sb.append("addUser() = {*.addUser()}\n");

			sb.append(this.addGlobalEvents(clContractFile));

			sb.append("\t}\n");// EVENTS END

			sb.append(this.addControllAutometa(clContractFile));
			sb.append("\n");

			sb.append(this.addAllmonitors(clContractFile));// PROPERTY START
			sb.append("\n");

			sb.append("}\n");// GLOBAL END

			FileWriter fstream = new FileWriter(fileName);
			BufferedWriter out = new BufferedWriter(fstream);
			out.write(sb.toString());
			// Close the output stream
			out.close();

		} catch (Exception e) {
			e.printStackTrace();
		}

	}

	public String convertCLToLARVA(String clContract, String methodName) {

		String str = null;
		try {
			this.appAnalyser.clearContract();

			this.appAnalyser.addClause(new Clause(clContract));

			this.appAnalyser.AnalyseContract(true);

			if (this.appAnalyser.getGraph().conflictFree()) {

				/*
				 * return
				 * this.appAnalyser.getGraph().generateAutomatonForLarva()
				 * .replaceFirst("clcontract", methodName);
				 */

				str = this.appAnalyser.getGraph().generateAutomatonForLarva()
						.replaceFirst("clcontract", methodName);
				str = str.replace(':', '_');
				str = str.replace(';', '_');
				
				//str = str.replace("\n", "\t\n");
				
				return str;
			}

		} catch (Exception e) {
			System.out.print("Problem in CL convertion");
		}

		return "";
	}

	public String addAllmonitors(String clFileName) {

		StringBuilder temp = new StringBuilder();

		CLMonitorList cml = new CLMonitorList(clFileName);

		for (int i = 0; i < cml.allMonitors.size(); i++) {

			temp.append("\n");
			temp.append(this.convertCLToLARVA(cml.allMonitors.get(i)
					.getClContact(), cml.allMonitors.get(i).getRelatedMethod()));

			// System.out.print(i+
			// " th monitor.............................start\n");
			/*
			 * System.out.print(this.convertCLToLARVA(cml.allMonitors.get(i)
			 * .getClContact(), cml.allMonitors.get(i).getRelatedMethod()));
			 */
			// System.out.print(i+
			// " th monitor.............................end\n");
			temp.append("\n");

		}

		return temp.toString();
	}

	// this will addchannel in larva script
	public String addChannel(String clFileName) {

		StringBuilder temp = new StringBuilder();

		CLMonitorList cml = new CLMonitorList(clFileName);

		for (int i = 0; i < cml.allMonitors.size(); i++) {

			// temp.append("\n");
			/*
			 * temp.append(this.convertCLToLARVA(cml.allMonitors.get(i)
			 * .getClContact(), cml.allMonitors.get(i).getRelatedMethod()));
			 */
			temp.append("\t\t");
			temp.append("Channel d" + (i + 1) + " = new Channel();");

			temp.append("\n");

		}

		return temp.toString();
	}

	// this will add controll variable in larva script
	public String addControllVariable(String clFileName) {

		StringBuilder temp = new StringBuilder();

		CLMonitorList cml = new CLMonitorList(clFileName);
		
		temp.append("\t\t");
		temp.append("boolean activate=true;\n");

		for (int i = 0; i < cml.allMonitors.size(); i++) {
			temp.append("\t\t");
			temp.append("boolean activate" + (i + 1) + " = false;");
			temp.append("\n");

		}

		return temp.toString();
	}

	// this will addchannel in larva script
	public String addGlobalEvents(String clFileName) {

		StringBuilder temp = new StringBuilder();
		StringBuilder tempOtherwise = new StringBuilder();

		CLMonitorList cml = new CLMonitorList(clFileName);

		// adding events
		for (int i = 0; i < cml.allMonitors.size(); i++) {

			// temp.append("\n");
			/*
			 * temp.append(this.convertCLToLARVA(cml.allMonitors.get(i)
			 * .getClContact(), cml.allMonitors.get(i).getRelatedMethod()));
			 */
			temp.append("\t\t");
			temp.append(cml.allMonitors.get(i).getRelatedMethod() + "()"
					+ " = {*." + cml.allMonitors.get(i).getRelatedMethod()
					+ "()}");

			temp.append("\n");

			// otherwise constraction
			//temp.append("\t\t");
			tempOtherwise.append("*."
					+ cml.allMonitors.get(i).getRelatedMethod() + "()|");

		}

		// adding Channels
		for (int i = 0; i < cml.allMonitors.size(); i++) {

			temp.append("\t\t");
			temp.append("channeld" + (i + 1) + "(String from" + (i + 1)
					+ ") = {d" + (i + 1) + ".receive(from" + (i + 1) + ")}");
			temp.append("\n");
		}
		temp.append("\t\t");
		temp.append("otherwise = {"
				+ tempOtherwise.substring(0, tempOtherwise.length() - 1) + "}");
		temp.append("\n");

		return temp.toString();
	}

	// this will controll autometa in larva script
	public String addControllAutometa(String clFileName) {

		StringBuilder temp = new StringBuilder();

		CLMonitorList cml = new CLMonitorList(clFileName);

		temp.append("\tPROPERTY MetaMonitor {\n");

		temp.append("\t\tSTATES {\n");

		temp.append("\t\t\tBAD { V{System.out.println(\"Forbidden!!!\");} }\n");

		temp.append("\t\t\tNORMAL {\n");

		/*
		 * for (int i = 0; i < cml.allMonitors.size(); i++) {
		 * temp.append("S"+(i+
		 * 1)+"{System.out.println(\""+cml.allMonitors.get(i).
		 * getRelatedMethod()+"!!!\");}\n"); }
		 */

		temp.append("\t\t\t\tS0{System.out.println(\"\\nMeta Monitor \\n\");}\n");

		temp.append("\t\t\t}\n");// normal

		temp.append("\t\t\tSTARTING {\n");// starting start

		temp.append("\t\t\t\tS0{}\n");

		temp.append("\t\t\t}\n");// starting end

		temp.append("\t\t}\n");// states end

		temp.append("\t\tTRANSITIONS {\n");// transition start

		// temp.append("S1 -> S2[login()\\d1.send(\"login\");]");

		for (int i = 0; i < cml.allMonitors.size(); i++) {
			/*
			 * temp.append("S" + (i + 1) + "{System.out.println(\"" +
			 * cml.allMonitors.get(i).getRelatedMethod() + "!!!\");}\n");
			 */
			
			temp.append("\t\t\t\t");
			temp.append("S0 -> S0[" + cml.allMonitors.get(i).getRelatedMethod()
					+ "()\\"+"activate==true"+"\\activate=false;activate"+(i + 1)+"=true;d" + (i + 1) + ".send(\""
					+ cml.allMonitors.get(i).getRelatedMethod() + "\");]\n");

		}

		// this line need to change
		temp.append("\t\t\t\t");
		temp.append("S0 ->V[request()\\"+"activate==true"+"\\System.out.println(\"Main Autometa reaches BAD state\");]\n");
		temp.append("\t\t}\n");// transition end

		temp.append("\t}\n");// property

		return temp.toString();
	}

	// this will add import into larva file from actual java system root
	// directory
	public String addImports(String javaSystemRootDirectory) {

		GetListOfFile glf = new GetListOfFile(javaSystemRootDirectory);

		// System.out.print(glf.getImports());

		return glf.getImports();
	}

}
